/LMAR=50/TMAR=50/RMAR=4095/BMAR=1/PMAR=0/XLINE=0/FONT#0=NGR13/USETI=0000025*TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX**TEX*

␈β↓R␈↓ ∧␈εαAN␈αINTERESTING␈αLISP␈αFUNCTION
␈βα1␈↓ α⊂␈εαIkuo␈α	Tak␈α␈euchi␈α	(1978)␈α
of␈α	the␈α
Electrical␈α	Comm␈α␈unication␈α
Laboratory␈α	of␈α	Nippon
␈βα]␈↓ ↓H␈εαTelephone␈α∂and␈α⊂Telegraph␈α∂Co.␈α⊂(Japan's␈α⊂Bell␈α∂Labs)␈α⊂devised␈α∂a␈α⊂recursiv␈α␈e␈α∂function
␈ββλ␈↓ ↓H␈εαprogram␈αfor␈αcomparing␈αthe␈αspeeds␈αof␈αLISP␈αsystems.␈αIt␈αcan␈αbe␈αmade␈αto␈αrun␈αa␈αlong
␈ββ3␈↓ ↓H␈εαtime␈αwithout␈αgenerating␈αlarge␈αn␈α␈um␈α␈bers␈αor␈αusing␈αm␈α␈uch␈αstack.␈αThe␈αprogram␈αis
␈β∧λ␈↓ α ␈ελt␈↓ α-␈ελa␈↓ α>␈ελk␈↓ αP␈εα(␈↓ α\␈ελx␈↓ αo␈εα,␈↓ α␈␈ελy␈↓ β∪␈εα,␈↓ β#␈ελz␈↓ β2␈εα)␈ε⊗␈α
 ␈↓ ∧α␈ε∩if␈↓ ∧$␈ελx␈↓ ∧A␈ε⊗∀␈↓ ∧o␈ελy␈↓ ¬∂␈ε∩then␈↓ ¬a␈ελy
␈β∧3␈↓ ∧α␈ε∩else␈↓ ∧F␈ελt␈↓ ∧S␈ελa␈↓ ∧e␈ελk␈↓ ∧w␈εα(␈↓ ¬β␈ελt␈↓ ¬⊂␈ελa␈↓ ¬"␈ελk␈↓ ¬4␈εα(␈↓ ¬@␈ελx␈↓ ¬Z␈ε⊗␈␈εα␈αλ1,␈↓ ε(␈ελy␈↓ ε<␈εα,␈↓ εL␈ελz␈↓ ε[␈εα),␈↓ εw␈ελt␈↓ π∧␈ελa␈↓ π⊗␈ελk␈↓ π(␈εα(␈↓ π4␈ελy␈↓ πP␈ε⊗␈␈εα␈αλ1,␈↓ λ≡␈ελz␈↓ λ-␈εα,␈↓ λ=␈ελx␈↓ λP␈εα),␈↓ λl␈ελt␈↓ λy␈ελa␈↓ 	␈ελk␈↓ 	≥␈εα(␈↓ 	)␈ελz␈↓ 	@␈ε⊗␈␈εα␈αλ1,␈↓ 
∞␈ελx␈↓ 
 ␈εα,␈↓ 
0␈ελy␈↓ 
E␈εα)),
␈β¬
␈↓ ↓H␈εαwhere␈αthe␈αvariables␈αmay␈αrange␈αo␈α␈v␈α␈er␈αthe␈αin␈α␈tegers␈α(including␈αnegativ␈α␈e)␈αor␈αelse␈αo␈α␈v␈α␈er
␈β¬9␈↓ ↓H␈εαreal␈α
n␈α␈um␈α␈bers.␈α⊃The␈α
program␈α∞has␈α
similar␈α∞properties␈α
in␈α∞the␈α
t␈α␈w␈α␈o␈α∞cases,␈α∞but␈α
pro␈α␈ving
␈β¬d␈↓ ↓H␈εαtermination␈απseems␈αλmore␈απtedious␈απif␈αλarbitrary␈απreal␈αλn␈α␈um␈α␈bers␈απare␈αλallo␈α␈w␈α␈ed.␈α
The␈απprogram
␈βε∂␈↓ ↓H␈εαhas␈αsev␈α␈eral␈αin␈α␈teresting␈αfeatures.
␈βε<␈↓ α⊂␈εα1.␈αInspection␈αsuggests␈αthat␈↓ ¬>␈ελt␈↓ ¬K␈ελa␈↓ ¬]␈ελk␈↓ ¬z␈εαsatis|es␈αthe␈αequation
␈βπ⊗␈↓ βx␈ελt␈↓ ∧¬␈ελa␈↓ ∧↔␈ελk␈↓ ∧(␈εα(␈↓ ∧4␈ελx␈↓ ∧O␈εα+␈↓ ∧{␈ελa␈↓ ¬
␈εα,␈↓ ¬≥␈ελy␈↓ ¬9␈εα+␈↓ ¬e␈ελa␈↓ ¬w␈εα,␈↓ επ␈ελz␈↓ ε≡␈εα+␈↓ εJ␈ελa␈↓ ε\␈εα)␈α
=␈↓ π ␈ελt␈↓ π-␈ελa␈↓ π?␈ελk␈↓ πQ␈εα(␈↓ π]␈ελx␈↓ πo␈εα,␈↓ π␈␈ελy␈↓ λ∀␈εα,␈↓ λ$␈ελz␈↓ λ3␈εα)␈αλ+␈↓ λs␈ελa␈↓ 	∧␈εα,
␈βπp␈↓ ↓H␈εαwhenev␈α␈er␈αthe␈α
computation␈α
terminates,␈α
and␈α
this␈α
can␈αbe␈α
sho␈α␈wn␈α
by␈α
subgoal␈αinduc-
␈βλ≤␈↓ ↓H␈εαtion.␈αNamely,␈α
it␈α	is␈α
true␈α	for␈α
the␈α	non-recursiv␈α␈e␈α
case,␈α
and␈α	assuming␈α
it␈α	for␈α
the␈α	referred
␈βλG␈↓ ↓H␈εαsets␈α
of␈αargumen␈α␈ts␈αyields␈αit␈α
for␈αthe␈αmain␈α
set.␈αA␈αformal␈αproof␈α
can␈αproceed␈αalong␈α
the
␈βλr␈↓ ↓H␈εαlines␈αsuggested␈αin␈α(McCarth␈α␈y␈α1978).␈αWe␈αdon't␈αuse␈αthis␈αfact␈αin␈αsubsequen␈α␈t␈αproofs.
␈β	∨␈↓ α⊂␈εα2.␈αExperimen␈α␈t␈αusing␈αLISP␈αindicates␈α|rst␈αof␈αall␈αthat␈αthe␈αvalue␈αof␈↓ 	⎇␈ελt␈↓ 

␈ελa␈↓ 
≠␈ελk␈↓ 
-␈εα(␈↓ 
9␈ελx␈↓ 
L␈εα,␈↓ 
\␈ελy␈↓ 
p␈εα,␈↓ ␈ελz␈↓ ∂␈εα)␈αis
␈β	J␈↓ ↓H␈εαalways␈αone␈αof␈↓ β*␈ελx␈↓ β<␈εα,␈↓ βR␈ελy␈↓ βs␈εαor␈↓ ∧∨␈ελz␈↓ ∧.␈εα.␈αI␈αdon't␈αsee␈αa␈αproof␈αof␈αthis␈αfact␈αin␈αisolation.
␈β	v␈↓ α⊂␈εα3.␈α
Lik␈α␈e␈α
the␈α91-function,␈α
the␈α
program␈αcomputes␈α
a␈αsimple␈α
non-recursiv␈α␈e␈αfunc-
␈β
"␈↓ ↓H␈εαtion.␈α∞Using␈α
LISP␈α
to␈αcompute␈α
some␈α
values␈α
of␈↓ π⊃␈ελt␈↓ π∨␈ελa␈↓ π0␈ελk␈↓ πO␈εαleads␈α
to␈α
the␈αguess␈α
that␈α
it␈α
is␈αthe
␈β
M␈↓ ↓H␈εαsame␈αas
␈β'␈↓ α|␈ελt␈↓ β	␈ελa␈↓ β≠␈ελk␈↓ β-␈εα0(␈↓ βK␈ελx␈↓ β]␈εα,␈↓ βm␈ελy␈↓ ∧↓␈εα,␈↓ ∧⊃␈ελz␈↓ ∧ ␈εα)␈α
=␈↓ ∧p␈ε∩if␈↓ ¬∩␈ελx␈↓ ¬/␈ε⊗∀␈↓ ¬]␈ελy␈↓ ¬⎇␈ε∩then␈↓ εO␈ελy␈↓ εo␈ε∩else␈αif␈↓ πU␈ελy␈↓ πs␈ε⊗∀␈↓ λ!␈ελz␈↓ λ<␈ε∩then␈↓ 	∞␈ελz␈↓ 	)␈ε∩else␈↓ 	m␈ελx␈↓ 
␈εα.
␈βα␈↓ ↓H␈εαSubstitution␈αλsho␈α␈ws␈αλthat␈↓ ∧?␈ελt␈↓ ∧L␈ελa␈↓ ∧↑␈ελk␈↓ ∧p␈εα0␈αλsatis|es␈αλthe␈αλfunctional␈αλequation␈α	for␈↓ 	-␈ελt␈↓ 	:␈ελa␈↓ 	L␈ελk␈↓ 	]␈εα,␈α	and␈αλtherefore
␈β-␈↓ ↓H␈εαby␈αthe␈ε ␈αminimization␈αschema␈εα␈αof␈α(McCarth␈α␈y␈α1978),
␈β
π␈↓ ∧␈␈ελt␈↓ ¬␈ελa␈↓ ¬≡␈ελk␈↓ ¬0␈εα(␈↓ ¬<␈ελx␈↓ ¬O␈εα,␈↓ ¬←␈ελy␈↓ ¬s␈εα,␈↓ εβ␈ελz␈↓ ε∩␈εα)␈α
=␈↓ εV␈ελt␈↓ εc␈ελa␈↓ εu␈ελk␈↓ ππ␈εα0(␈↓ π%␈ελx␈↓ π8␈εα,␈↓ πH␈ελy␈↓ π\␈εα,␈↓ πl␈ελz␈↓ π{␈εα)
␈β
b␈↓ ↓H␈εαwhenev␈α␈er␈αthe␈α
former␈α
terminates.␈ε ␈α∞A␈αfortiori␈εα,␈α
this␈α
establishes␈α
that␈↓ 	B␈ελt␈↓ 	O␈ελa␈↓ 	a␈ελk␈↓ 	s␈εα(␈↓ 	␈␈ελx␈↓ 
∩␈εα,␈↓ 
"␈ελy␈↓ 
6␈εα,␈↓ 
F␈ελz␈↓ 
U␈εα)␈αtak␈α␈es
␈β∞
␈↓ ↓H␈εαone␈αof␈αthe␈αvariables␈αas␈αvalue,␈αbut␈αmaybe␈αthat␈αfact␈αcould␈αbe␈αpro␈α␈v␈α␈ed␈αseparately.
␈β∞9␈↓ α⊂␈εα4.␈αIn␈α	order␈α	to␈α	pro␈α␈v␈α␈e␈α	that␈↓ ¬∞␈ελt␈↓ ¬≠␈ελa␈↓ ¬,␈ελk␈↓ ¬G␈εαis␈α	total,␈α
w␈α␈e␈α	write␈α	a␈ε ␈α	\derived␈α	program"␈↓ 
␈ελd␈↓ 
 ␈ελt␈↓ 
-␈ελa␈↓ 
?␈ελk␈↓ 
Q␈εα(␈↓ 
]␈ελx␈↓ 
o␈εα,␈↓ 
␈␈ελy␈↓ ∪␈εα,␈↓ #␈ελz␈↓ 2␈εα)
␈β∞e␈↓ ↓H␈εαthat␈α
computes␈α
the␈α
depth␈α
of␈α
recursion␈α
in␈α␈v␈α␈olv␈α␈ed␈α
in␈αcomputing␈↓ λx␈ελt␈↓ 	¬␈ελa␈↓ 	↔␈ελk␈↓ 	(␈εα(␈↓ 	4␈ελx␈↓ 	G␈εα,␈↓ 	W␈ελy␈↓ 	k␈εα,␈↓ 	{␈ελz␈↓ 

␈εα)␈α
using␈α
call-
␈β∂.␈↓ ε:␈εα1
␈β⊃∂

␈β↓R␈↓ ↓H␈εαby-value.␈αWe␈αhav␈α␈e
␈βα≤␈↓ ↓I␈ελd␈↓ ↓]␈ελt␈↓ ↓j␈ελa␈↓ ↓|␈ελk␈↓ α∞␈εα(␈↓ α~␈ελx␈↓ α,␈εα,␈↓ α<␈ελy␈↓ αQ␈εα,␈↓ αa␈ελz␈↓ αp␈εα)␈ε⊗␈α
 ␈↓ β@␈ε∩if␈↓ βb␈ελx␈↓ β}␈ε⊗∀␈↓ ∧,␈ελy␈↓ ∧L␈ε∩then␈↓ ¬≡␈εα0
␈βαG␈↓ β@␈ε∩else␈↓ ∧∧␈εα1␈αλ+␈↓ ∧J␈εαmax␈↓ ¬∞␈εα(␈↓ ¬~␈ελd␈↓ ¬.␈ελt␈↓ ¬;␈ελa␈↓ ¬M␈ελk␈↓ ¬↑␈εα(␈↓ ¬j␈ελx␈↓ ε¬␈ε⊗␈␈εα␈αλ1,␈↓ εS␈ελy␈↓ εg␈εα,␈↓ εw␈ελz␈↓ πε␈εα),
␈βαr␈↓ ¬~␈ελd␈↓ ¬.␈ελt␈↓ ¬;␈ελa␈↓ ¬M␈ελk␈↓ ¬↑␈εα(␈↓ ¬j␈ελy␈↓ εε␈ε⊗␈␈εα␈αλ1,␈↓ εT␈ελx␈↓ εg␈εα,␈↓ εw␈ελz␈↓ πε␈εα),
␈ββ≡␈↓ ¬~␈ελd␈↓ ¬.␈ελt␈↓ ¬;␈ελa␈↓ ¬M␈ελk␈↓ ¬↑␈εα(␈↓ ¬j␈ελz␈↓ ε↓␈ε⊗␈␈εα␈αλ1,␈↓ εO␈ελx␈↓ εb␈εα,␈↓ εr␈ελy␈↓ πε␈εα),
␈ββI␈↓ ¬~␈ελd␈↓ ¬.␈ελt␈↓ ¬;␈ελa␈↓ ¬M␈ελk␈↓ ¬↑␈εα(␈↓ ¬j␈ελt␈↓ ¬w␈ελa␈↓ ε	␈ελk␈↓ ε≠␈εα(␈↓ ε'␈ελx␈↓ εB␈ε⊗␈␈εα␈αλ1,␈↓ π⊂␈ελy␈↓ π$␈εα,␈↓ π4␈ελz␈↓ πC␈εα),␈↓ π←␈ελt␈↓ πl␈ελa␈↓ π}␈ελk␈↓ λ⊂␈εα(␈↓ λ≤␈ελy␈↓ λ8␈ε⊗␈␈εα␈αλ1,␈↓ 	ε␈ελz␈↓ 	∃␈εα,␈↓ 	%␈ελx␈↓ 	8␈εα),␈↓ 	T␈ελt␈↓ 	a␈ελa␈↓ 	r␈ελk␈↓ 
∧␈εα(␈↓ 
⊂␈ελz␈↓ 
'␈ε⊗␈␈εα␈αλ1,␈↓ 
u␈ελx␈↓ λ␈εα,␈↓ _␈ελy␈↓ ,␈εα))).
␈β∧∪␈↓ ↓H␈εαExperimen␈α␈t␈αwith␈αLISP␈αleads␈αto␈αthe␈αconjecture␈αthat␈αfor␈αin␈α␈teger␈αvalues␈αof␈αthe␈αvari-
␈β∧>␈↓ ↓H␈εαables,␈↓ α,␈ελd␈↓ α@␈ελt␈↓ αM␈ελa␈↓ α←␈ελk␈↓ α|␈εαis␈αextensionally␈αequivalen␈α␈t␈αto
␈β¬∞␈↓ ∧≡␈ελd␈↓ ∧2␈ελt␈↓ ∧?␈ελa␈↓ ∧Q␈ελk␈↓ ∧c␈εα0(␈↓ ¬↓␈ελx␈↓ ¬∀␈εα,␈↓ ¬$␈ελy␈↓ ¬8␈εα,␈↓ ¬H␈ελz␈↓ ¬W␈εα)␈α
=␈↓ ε≠␈ελd␈↓ ε/␈ελt␈↓ ε<␈ελa␈↓ εN␈ελk␈↓ ε`␈εα00(␈↓ π⊂␈ελx␈↓ π+␈ε⊗␈␈↓ πW␈ελy␈↓ πk␈εα,␈↓ π{␈ελz␈↓ λ∩␈ε⊗␈␈↓ λ>␈ελy␈↓ λR␈εα),
␈β¬↑␈↓ ↓H␈εαwhere
␈βε"␈↓ αg␈ελd␈↓ α|␈ελt␈↓ β	␈ελa␈↓ β≠␈ελk␈↓ β,␈εα00(␈↓ β\␈ελm␈↓ β|␈εα,␈↓ ∧␈ελn␈↓ ∧"␈εα)␈α
=␈↓ ∧r␈ε∩if␈↓ ¬∀␈ελm␈↓ ¬=␈ε⊗∀␈εα␈α
0␈↓ ε	␈ε∩then␈↓ ε[␈εα0
␈βεM␈↓ ∧r␈ε∩else␈αif␈↓ ¬X␈ελn␈↓ ¬w␈ε⊗∃␈εα␈α
2␈↓ εC␈ε∩then␈↓ π∃␈ελm␈↓ π=␈εα+␈↓ πi␈ελn␈↓ π␈␈εα(␈↓ λ␈ελn␈↓ λ(␈ε⊗␈␈εα␈αλ1)/2␈ε⊗␈αλ␈␈εα␈αλ1
␈βεx␈↓ ∧r␈ε∩else␈αif␈↓ ¬X␈ελn␈↓ ¬w␈ε⊗∃␈εα␈α
0␈↓ εC␈ε∩then␈↓ π∃␈ελm
␈βπ#␈↓ ∧r␈ε∩else␈αif␈↓ ¬X␈ελn␈↓ ¬w␈εα=␈ε⊗␈α
␈␈εα1␈↓ εg␈ε∩then␈↓ π9␈εα(␈↓ πE␈ελm␈↓ πm␈εα+␈αλ1)(␈↓ λC␈ελm␈↓ λk␈εα+␈αλ2)/2␈ε⊗␈αλ␈␈εα␈αλ1
␈βπN␈↓ ∧r␈ε∩else␈↓ ¬6␈εα(␈↓ ¬B␈ελm␈↓ ¬i␈ε⊗␈␈↓ ε∃␈ελn␈↓ ε+␈εα)(␈↓ εC␈ελm␈↓ εk␈ε⊗␈␈↓ π↔␈ελn␈↓ π4␈εα+␈αλ1)/2␈ε⊗␈αλ␈␈↓ λV␈ελm␈↓ λ}␈ε⊗␈␈εα␈αλ1.
␈βλ≡␈↓ ↓H␈εαWe␈α
don't␈α
bother␈αto␈α
v␈α␈erify␈α
the␈αconjecture.␈αInstead␈αw␈α␈e␈α
use␈↓ λB␈ελd␈↓ λV␈ελt␈↓ λc␈ελa␈↓ λu␈ελk␈↓ 	π␈εα0␈α
as␈αa␈α
rank␈α
function
␈βλJ␈↓ ↓H␈εαto␈αpro␈α␈v␈α␈e␈ε⊗␈α8␈↓ αj␈ελi␈↓ αx␈εα.λ(␈↓ β(␈ελi␈↓ β5␈εα)␈αby␈αcourse-of-values␈αinduction␈αwhere
␈β	~␈↓ αg␈εαλ(␈↓ β
␈ελi␈↓ β≠␈εα)␈ε⊗␈α
⊃␈α
8␈↓ βs␈ελx␈↓ ∧ε␈ελy␈↓ ∧~␈ελz␈↓ ∧)␈εα.(␈↓ ∧?␈ελd␈↓ ∧S␈ελt␈↓ ∧`␈ελa␈↓ ∧r␈ελk␈↓ ¬∧␈εα0(␈↓ ¬"␈ελx␈↓ ¬5␈εα,␈↓ ¬E␈ελy␈↓ ¬Y␈εα,␈↓ ¬i␈ελz␈↓ ¬x␈εα)␈α
=␈↓ ε<␈ελi␈↓ εT␈ε⊗≠␈↓ πα␈ελt␈↓ π∂␈ελa␈↓ π!␈ελk␈↓ π2␈εα(␈↓ π>␈ελx␈↓ πQ␈εα,␈↓ πa␈ελy␈↓ πu␈εα,␈↓ λ¬␈ελz␈↓ λ∀␈εα)␈α
=␈↓ λX␈ελt␈↓ λe␈ελa␈↓ λw␈ελk␈↓ 		␈εα0(␈↓ 	'␈ελx␈↓ 	:␈εα,␈↓ 	J␈ελy␈↓ 	↑␈εα,␈↓ 	n␈ελz␈↓ 	⎇␈εα)).
␈β	j␈↓ ↓H␈εαSince␈αw␈α␈e␈αalready␈αkno␈α␈w␈αthat␈↓ ¬ε␈ελt␈↓ ¬∪␈ελa␈↓ ¬%␈ελk␈↓ ¬7␈εα0␈αsatis|es␈αthe␈αfunctional␈αequation␈αof␈↓ 	{␈ελt␈↓ 
λ␈ελa␈↓ 
~␈ελk␈↓ 
,␈εα,␈αw␈α␈e␈αneed
␈β
∃␈↓ ↓H␈εαonly␈αλsho␈α␈w␈αλthat␈α	in␈αλthe␈αλrecursiv␈α␈e␈αλcase␈α	of␈↓ ε⊗␈ελt␈↓ ε#␈ελa␈↓ ε5␈ελk␈↓ εG␈εα,␈α	i.e.␈αwhen␈↓ πm␈ελx␈↓ λ
␈εα>␈↓ λ8␈ελy␈↓ λL␈εα,␈α	the␈αλreferred␈αλargumen␈α␈ts
␈β
@␈↓ ↓H␈εαare␈α
of␈αlo␈α␈w␈α␈er␈αrank␈α
than␈αthe␈αmain␈α
ones.␈αTh␈α␈us␈αw␈α␈e␈α
m␈α␈ust␈αsho␈α␈w␈αthat␈α
each␈αof␈↓ 
∨␈ελd␈↓ 
3␈ελt␈↓ 
@␈ελa␈↓ 
R␈ελk␈↓ 
c␈εα0(␈↓ ↓␈ελx␈↓ ~␈ε⊗␈
␈β
k␈↓ ↓H␈εα1,␈↓ ↓j␈ελy␈↓ ↓}␈εα,␈↓ α∞␈ελz␈↓ α≥␈εα),␈↓ α?␈ελd␈↓ αS␈ελt␈↓ α`␈ελa␈↓ αr␈ελk␈↓ β∧␈εα0(␈↓ β"␈ελy␈↓ β>␈ε⊗␈␈εα␈αλ1,␈↓ ∧␈ελz␈↓ ∧≠␈εα,␈↓ ∧+␈ελx␈↓ ∧=␈εα),␈↓ ∧←␈ελd␈↓ ∧t␈ελt␈↓ ¬↓␈ελa␈↓ ¬∪␈ελk␈↓ ¬$␈εα0(␈↓ ¬B␈ελz␈↓ ¬Y␈ε⊗␈␈εα␈αλ1,␈↓ ε'␈ελx␈↓ ε:␈εα,␈↓ εJ␈ελy␈↓ ε↑␈εα),␈αand␈↓ πF␈ελd␈↓ πZ␈ελt␈↓ πg␈ελa␈↓ πy␈ελk␈↓ λ␈εα0(␈↓ λ)␈ελt␈↓ λ6␈ελa␈↓ λH␈ελk␈↓ λZ␈εα0(␈↓ λx␈ελx␈↓ 	∪␈ε⊗␈␈εα␈αλ1,␈↓ 	a␈ελy␈↓ 	u␈εα,␈↓ 
¬␈ελz␈↓ 
∀␈εα),␈↓ 
0␈ελt␈↓ 
=␈ελa␈↓ 
O␈ελk␈↓ 
`␈εα0(␈↓ 
}␈ελy␈↓ ~␈ε⊗␈
␈β⊗␈↓ ↓H␈εα1,␈↓ ↓j␈ελz␈↓ ↓y␈εα,␈↓ α	␈ελx␈↓ α≠␈εα),␈↓ α7␈ελt␈↓ αD␈ελa␈↓ αV␈ελk␈↓ αh␈εα0(␈↓ βε␈ελz␈↓ β≡␈ε⊗␈␈εα␈αλ1,␈↓ βl␈ελx␈↓ β␈␈εα,␈↓ ∧∂␈ελy␈↓ ∧#␈εα)␈αis␈α
strictly␈α
less␈αthan␈↓ εt␈ελd␈↓ πλ␈ελt␈↓ π∃␈ελa␈↓ π'␈ελk␈↓ π9␈εα0(␈↓ πW␈ελx␈↓ πi␈εα,␈↓ πy␈ελy␈↓ λ
␈εα,␈↓ λ≥␈ελz␈↓ λ,␈εα).␈α∞Each␈α
inequality␈αfollo␈α␈ws
␈βB␈↓ ↓H␈εαfrom␈α
a␈α
separate␈α
easy␈α
case␈α
analysis.␈α∂Presumably␈α
termination␈αcould␈α
be␈α
pro␈α␈v␈α␈ed␈α
for
␈βm␈↓ ↓H␈εαthe␈αnon-in␈α␈teger␈αcase␈α
by␈αa␈αsimilar␈α
argumen␈α␈t␈αwith␈αa␈αmore␈α
complicated␈αform␈α␈ula␈αfor
␈β_␈↓ ↓H␈ελd␈↓ ↓\␈ελt␈↓ ↓i␈ελa␈↓ ↓{␈ελk␈↓ α␈εα00.␈αWe␈αleav␈α␈e␈αthis␈αas␈αan␈αex␈α␈ercise␈αfor␈αthe␈αreader.
␈βC␈↓ α⊂␈εα5.␈αLik␈α␈e␈αMorris's␈αprogram
␈β
∪␈↓ αM␈ελm␈↓ αl␈ελo␈↓ α{␈ελr␈↓ β␈ελr␈↓ β≠␈ελi␈↓ β)␈ελs␈↓ β8␈εα(␈↓ βD␈ελx␈↓ βW␈εα,␈↓ βg␈ελy␈↓ β{␈εα)␈ε⊗␈α
 ␈↓ ∧K␈ε∩if␈↓ ∧m␈ελx␈↓ ¬	␈εα=␈α
0␈↓ ¬U␈ε∩then␈↓ ε'␈εα1␈↓ εE␈ε∩else␈↓ π	␈ελm␈↓ π)␈ελo␈↓ π8␈ελr␈↓ πH␈ελr␈↓ πX␈ελi␈↓ πf␈ελs␈↓ πu␈εα(␈↓ λ↓␈ελx␈↓ λ≠␈ε⊗␈␈εα␈αλ1,␈↓ λi␈ελm␈↓ 		␈ελo␈↓ 	_␈ελr␈↓ 	(␈ελr␈↓ 	8␈ελi␈↓ 	F␈ελs␈↓ 	U␈εα(␈↓ 	a␈ελx␈↓ 	s␈εα,␈↓ 
β␈ελy␈↓ 
↔␈εα)),
␈β
c␈↓ ↓H␈ελt␈↓ ↓U␈ελa␈↓ ↓g␈ελk␈↓ α∧␈εαis␈αmore␈αquickly␈αcomputed␈αby␈αcall-by-need␈α(Vuillemin␈α1973).␈αIn␈αfact␈αthe␈αn␈α␈um-
␈β∞∞␈↓ ↓H␈εαber␈α
of␈α
function␈α
calls␈α∞appears␈α
to␈α
be␈α
exponen␈α␈tial␈α∞with␈α
call-by-value␈α
and␈α
quadratic
␈β∞9␈↓ ↓H␈εαwith␈α∂call-by-need.␈α↔The␈α∂culprit␈α⊂is␈α∂the␈α⊂third␈α∂argumen␈α␈t␈α⊂of␈α∂the␈α⊂outer␈α∂call,␈α⊂namely
␈β∞e␈↓ ↓H␈ελt␈↓ ↓U␈ελa␈↓ ↓g␈ελk␈↓ ↓x␈εα(␈↓ α∧␈ελz␈↓ α≠␈ε⊗␈␈εα␈αλ1,␈↓ αi␈ελx␈↓ α|␈εα,␈↓ β␈ελy␈↓ β ␈εα)␈αwhich␈αis␈αoften␈αunneeded.␈αUnlik␈α␈e␈↓ π;␈ελm␈↓ π[␈ελo␈↓ πj␈ελr␈↓ πz␈ελr␈↓ λ	␈ελi␈↓ λ↔␈ελs␈↓ λ&␈εα,␈αho␈α␈w␈α␈ev␈α␈er,␈↓ 	Q␈ελt␈↓ 	↑␈ελa␈↓ 	p␈ελk␈↓ 
∞␈εαis␈αtotal.
␈β∂.␈↓ ε:␈εα2
␈β⊃∂

␈β↓R␈↓ α⊂␈εαA␈αcall-by-need␈αv␈α␈ersion␈αof␈↓ ¬%␈ελt␈↓ ¬2␈ελa␈↓ ¬D␈ελk␈↓ ¬a␈εαis␈αgiv␈α␈en␈αby
␈βα(␈↓ ∧o␈ελn␈↓ ¬¬␈ελt␈↓ ¬∩␈ελa␈↓ ¬$␈ελk␈↓ ¬6␈εα(␈↓ ¬B␈ελx␈↓ ¬T␈εα,␈↓ ¬d␈ελy␈↓ ¬x␈εα,␈↓ ελ␈ελz␈↓ ε↔␈εα)␈ε⊗␈α
 ␈↓ ε[␈ελv␈↓ εn␈ελt␈↓ ε{␈ελa␈↓ π
␈ελk␈↓ π∨␈ε⊗h␈↓ π+␈ελx␈↓ π>␈εα,␈↓ πN␈ελy␈↓ πb␈εα,␈↓ πr␈ελz␈↓ λ↓␈ε⊗i␈εα,
␈βα}␈↓ ↓H␈εαwhere
␈ββF␈↓ ↓P␈ελv␈↓ ↓c␈ελt␈↓ ↓p␈ελa␈↓ αα␈ελk␈↓ α≠␈ελu␈↓ α;␈ε⊗ ␈↓ αu␈ε∩if␈↓ β↔␈ελn␈↓ β-␈ελu␈↓ βB␈ελm␈↓ βb␈ελb␈↓ βp␈ελe␈↓ β␈␈ελr␈↓ ∧∞␈ελp␈↓ ∧'␈ελu␈↓ ∧H␈ε∩then␈↓ ¬~␈ελu
␈ββq␈↓ αu␈ε∩else␈αif␈↓ β[␈ε∩n␈↓ β{␈ε∩d␈↓ ∧≠␈ελu␈↓ ∧=␈ε∩then␈↓ ¬∂␈ελv␈↓ ¬!␈ελt␈↓ ¬/␈ελa␈↓ ¬@␈ελk␈↓ ¬R␈εα(␈↓ ¬j␈ε∩a␈↓ ελ␈ελu␈↓ ε≡␈εα)␈ε⊗␈αλ␈␈εα␈αλ1
␈β∧≥␈↓ αu␈ε∩else␈↓ β9␈ε⊗f␈↓ βK␈ελv␈↓ β↑␈ελt␈↓ βk␈ελa␈↓ β⎇␈ελk␈↓ ∧≠␈ε∩a␈↓ ∧9␈ελu␈↓ ∧N␈εα,␈↓ ∧↑␈ελv␈↓ ∧q␈ελt␈↓ ∧}␈ελa␈↓ ¬⊂␈ελk␈↓ ¬.␈ε∩ad␈↓ ¬`␈ελu␈↓ ¬u␈ε⊗g␈εα[␈↓ ε⊃␈ελ∃␈↓ ε&␈ελx␈↓ ε9␈ελy␈↓ εM␈εα.
␈β∧H␈↓ β=␈ε∩if␈↓ β←␈ελx␈↓ β|␈ε⊗∀␈↓ ∧*␈ελy␈↓ ∧J␈ε∩then␈↓ ¬≤␈ελy
␈β∧s␈↓ β=␈ε∩else␈↓ ∧↓␈ελv␈↓ ∧∀␈ελt␈↓ ∧!␈ελa␈↓ ∧3␈ελk␈↓ ∧E␈ε⊗hh␈↓ ∧]␈ελx␈↓ ∧w␈ε⊗␈␈εα␈αλ1,␈↓ ¬E␈ελy␈↓ ¬Y␈εα,␈↓ ¬u␈ε∩add␈↓ ε;␈ελu␈↓ εQ␈ε⊗i␈εα,␈ε⊗␈αεh␈↓ εy␈ελy␈↓ π∃␈ε⊗␈␈εα␈αλ1,␈↓ πo␈ε∩add␈↓ λ5␈ελu␈↓ λK␈εα,␈↓ λ[␈ελx␈↓ λn␈ε⊗i␈εα,␈ε⊗␈αεh␈↓ 	"␈ε∩add␈↓ 	h␈ελu␈↓ 
¬␈ε⊗␈␈εα␈αλ1,␈↓ 
S␈ελx␈↓ 
f␈εα,␈↓ 
v␈ελy␈↓ 
␈ε⊗ii␈εα].
␈β¬I␈↓ ↓H␈ελv␈↓ ↓Z␈ελt␈↓ ↓g␈ελa␈↓ ↓y␈ελk␈↓ α≤␈εαis␈α⊂obtained␈α⊃from␈↓ ∧7␈ελt␈↓ ∧D␈ελa␈↓ ∧V␈ελk␈↓ ∧x␈εαin␈α⊃a␈α⊂somewhat␈α⊃ad␈α⊂hoc␈α⊃way.␈α→Since␈α⊂w␈α␈e␈α⊃don't␈α⊂always
␈β¬u␈↓ ↓H␈εαcompute␈α	all␈α	argumen␈α␈ts␈α	of␈α	a␈α	function␈α	w␈α␈e␈α	m␈α␈ust␈α	w␈α␈ork␈α	with␈α	triples␈α	whose␈α	elemen␈α␈ts␈α	are
␈βε ␈↓ ↓H␈εαeither␈α	n␈α␈um␈α␈bers␈α
or␈α
applications␈α
of␈α
functions␈α
to␈α
argumen␈α␈ts.␈αThe␈α
only␈α
functions␈α	that
␈βεK␈↓ ↓H␈εαoccur␈α
are␈↓ αg␈ελv␈↓ αz␈ελt␈↓ βπ␈ελa␈↓ β→␈ελk␈↓ β8␈εαitself␈α∞and␈α
subtracting␈α∞one.␈α⊃Therefore,␈α∞a␈α∞n␈α␈um␈α␈ber␈α
stands␈α∞for␈α
itself,
␈βεv␈↓ ↓H␈εαan␈α	application␈α
of␈↓ βW␈ελv␈↓ βj␈ελt␈↓ βw␈ελa␈↓ ∧	␈ελk␈↓ ∧$␈εαis␈α
represen␈α␈ted␈α
by␈α
a␈α
triple,␈α
and␈α
an␈α
application␈α
of␈α	subtracting
␈βπ!␈↓ ↓H␈εαone␈αis␈αrepresen␈α␈ted␈αby␈αa␈αlist␈αof␈αone␈αelemen␈α␈t←the␈αinner␈αexpression␈αfrom␈αwhich␈αone
␈βπM␈↓ ↓H␈εαis␈α
to␈αbe␈αsubtracted.␈αPerhaps␈αI'm␈αbeing␈α
thick,␈αbut␈αit␈αseems␈α
to␈αme␈αthat␈α
call-by-need
␈βπx␈↓ ↓H␈εαrequires␈αlists␈αor␈αat␈αleast␈αputting␈αsym␈α␈bols␈αon␈αthe␈αstack.
␈βλ#␈↓ α⊂␈εαMA␈α␈CLISP␈αv␈α␈ersions␈α
of␈↓ ∧t␈ελt␈↓ ¬↓␈ελa␈↓ ¬∪␈ελk␈↓ ¬2␈εαand␈αfriends␈α
are␈α
in␈α
the␈α
|le␈α
T␈α⎇AK.LSP[F78,JMC]␈αat
␈βλN␈↓ ↓H␈εαSU-AI.␈αI␈α
thank␈αDon␈α
Kn␈α␈uth␈α
for␈αsuggesting␈α
call-by-need.␈α∞The␈αexternal␈α
or␈αpublica-
␈βλy␈↓ ↓H␈εαtion␈α∂LISP␈α∂notation␈α∂is␈α∂as␈α∂in␈α∂(McCarth␈α␈y␈α∂and␈α⊂Talcott␈α∂1978).␈α∃It␈α∂has␈α∂the␈α∂follo␈α␈wing
␈β	%␈↓ ↓H␈εαfeatures:␈α
(1)␈↓ β≡␈ε∩a␈↓ β<␈εαand␈↓ ∧β␈ε∩d␈↓ ∧#␈εαare␈α
used␈α
for␈↓ ¬l␈ελc␈↓ ¬z␈ελa␈↓ ε␈ελr␈↓ ε)␈εαand␈↓ εp␈ελc␈↓ ε}␈ελd␈↓ π∩␈ελr␈↓ π"␈εα,␈α
and␈α
their␈α
compounds␈α
are␈αformed
␈β	P␈↓ ↓H␈εαsimilarly.␈α(2)␈α
The␈α	in|x␈α
.␈α	is␈α
used␈α
for␈↓ ¬j␈ελc␈↓ ¬y␈ελo␈↓ ελ␈ελn␈↓ ε≥␈ελs␈↓ ε,␈εα,␈α
and␈ε⊗␈α
h␈↓ π⊂␈ελx␈↓ π#␈εα,␈↓ π3␈ελy␈↓ πG␈εα,␈↓ πW␈εα.␈αε.␈αε.␈↓ λ↓␈εα,␈↓ λ⊃␈ελz␈↓ λ ␈ε⊗i␈εα␈α
is␈α	used␈α
for␈↓ 	\␈ελl␈↓ 	g␈ελi␈↓ 	u␈ελs␈↓ 
∧␈ελt␈↓ 
⊃␈εα[␈↓ 
≠␈ελx␈↓ 
-␈εα,␈↓ 
=␈ελy␈↓ 
Q␈εα,␈↓ 
a␈εα.␈αε.␈αε.␈↓ ␈εα,␈↓ ≠␈ελz␈↓ *␈εα].
␈β	{␈↓ ↓H␈εα(3)␈ε⊗␈α	f␈↓ α
␈ελx␈↓ α∨␈εα,␈↓ α/␈ελy␈↓ αC␈εα,␈↓ αS␈εα.␈αε.␈αε.␈↓ α⎇␈εα,␈↓ β
␈ελz␈↓ β≤␈ε⊗g␈↓ β.␈ελf␈↓ βI␈εαis␈α	used␈α	for␈↓ ∧n␈ελf␈↓ ∧␈␈εα[␈↓ ¬	␈ελx␈↓ ¬≤␈εα,␈↓ ¬,␈ελy␈↓ ¬@␈εα,␈↓ ¬P␈εα.␈αε.␈αε.␈↓ ¬z␈εα,␈↓ ε
␈ελz␈↓ ε→␈εα]␈α	whenev␈α␈er␈α	w␈α␈e␈α	prefer␈α	to␈α	write␈αλthe␈α	argumen␈α␈ts
␈β
&␈↓ ↓H␈εα|rst␈αand␈αthe␈αfunction␈αname␈αlater.
␈β
u␈↓ α⊂␈ε∩References
␈β+␈↓ ↓H␈εα(McCarth␈α␈y␈α1978)␈α~John␈αMcCarth␈α␈y,␈αRepresen␈α␈tation␈αof␈α
recursiv␈α␈e␈αprograms␈αin␈α|rst
␈βW␈↓ α⊂␈εαorder␈αλlogic,␈ε ␈α	Proceedings␈αλof␈αλthe␈α	International␈αλConference␈αλon␈αλMathematical␈αλStudies
␈βα␈↓ α⊂␈ε of␈αInformation␈αProcessing␈εα,␈αKy␈α␈oto,␈αAugust␈α1978,␈α587↑605.
␈β8␈↓ ↓H␈εα(McCarth␈α␈y␈αand␈αTalcott␈α
1978)␈α→John␈α
McCarth␈α␈y␈αand␈αCarolyn␈α
Talcott,␈ε∩␈αLISP:␈αPro-
␈βc␈↓ α⊂␈ε∩gramming␈αand␈αPro␈α␈ving␈εα,␈αpreliminary␈αedition,␈αComputer␈αScience␈αDepartmen␈α␈t,
␈β
∞␈↓ α⊂␈εαStanford␈αUniv␈α␈ersity,␈α1978.
␈β
D␈↓ ↓H␈εα(Tak␈α␈euchi␈α1978)␈α→Ikuo␈αTak␈α␈euchi,␈αpersonal␈αcomm␈α␈unication.
␈β
q␈↓ ∧6␈εα∞
␈β
z␈↓ ↓H␈εα(Vuillemin␈α
1973)␈α↔Jean␈↓ ∧3␈εαE␈↓ ∧K␈εαtienne␈αVuillemin,␈ε ␈αProof␈αtechniques␈αfor␈αrecursive␈α
programs␈εα,
␈β∞%␈↓ α⊂␈εαPh.D.␈αthesis,␈αComputer␈αScience␈αDepartmen␈α␈t,␈αStanford␈αUniv␈α␈ersity,␈α1973.
␈β∂.␈↓ ε:␈εα3
␈β⊃∂/FONT#2=cmr10[XGP,SYS]=λ∞'()+,-./0123456789:=>ABCDEFGIJKLMNOPRSTUVW[]↑←abcdefghijklmnopqrstuvwxy||/FONT#8=cmi10[XGP,SYS]=∃abcdefiklmnoprstuvxyzz/FONT#18=cmb10[XGP,SYS]=-:ILPRSacdefghilmnorstvv/FONT#22=cmsy10[XGP,SYS]=⊃∀∃≠ 8fghii/FONT#32=cmti10[XGP,SYS]="ACIMPS\acdefghilmnopqrstuvzz